COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	FETCH INTEG2.AX
C00003 ENDMK
C⊗;
FETCH INTEG2.AX;
DECLARE PREDPAR Q(NATNUM);
∧I INDUCTION[P←λK.(∀N.(K≥N ∧ Q(N) ⊃ ∃N1.(Q(N1) ∧ ∀M.(¬(M≥N1) ⊃ ¬Q(M)))))];
∀E GREATER1 M;
TAUT ¬(M≥0)⊃¬Q(M) 2;
∀I 3 M;
ASSUME Q(0);
∧I 5 4;
∃I 6 0←N1;
∀E GREATER2 N;
⊃I 5 7;
TAUTEQ 0≥N ∧ Q(N) ⊃ 7: 8 9;
∀I 10 N;
TAUT 1:#1#2⊃1:#2 1 11;

ASSUME 12:#1#1#1;
ASSUME Q(SUCC N);
ASSUME ∀M.(¬(M ≥ SUCC N) ⊃ ¬Q(M));
∧I 14 15;
∃I 16 SUCC N ← N1;